es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id} ,
Q:({e:E| loc(e) = loc(e1)  Id} {e:E| loc(e) = loc(e1)  Id} ).
e1 loc e2   Q(e1,e2)  [e1,e2]~([a,b].Q(a,b))+ 

latex

Definitions	t  T, x:A. B(x), , loc(e), Id, E, e loc e' , x(s1,s2), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), P  Q, ES, [e1,e2]~([a,b].p(a;b))+
Lemmas	es-pstar-q-trivial, event system wf, es-E wf, Id wf, es-loc wf